c formula generated with seed 1, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.410000
c the planted solution is {1, 8, 9, 10, 13, 15, 16, 17, 18, 19, 22, 27, 28, 30, 31, 32, 33, 36, 38, 40, 41, 43, 46, 47, 49, 50, 55, 56, 57, 58, 61, 66, 71, 73, 78, 82, 84, 85, 89, 91, 94, 95, 96, 97, 98, 104, 109, 111, 112, 113, 115, 117, 124, 125, 127, 133, 134, 135, 137, 138, 139, 140, 141, 146, 147, 150, 151, 152, 153, 154, 155, 159, 162, 163, 166, 167, 169, 170, 171, 173, 175, 178, 179, 180, 181, 182, 184, 185, 186, 191, 192, 195, 196, 201, 202, 205, 207, 210, 211, 215, 216, 217, 218, 220, 222, 224, 225, 226, 227, 228, 233, 235, 238, 239, 242, 243, 244, 246, 247, 248, 249, 250, 251, 253, 254, 256, 258, 259, 260, 262, 263, 266, 268, 272, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 290, 291, 292, 294, 295, 297, 298, 299, 300, 303, 308, 311, 312, 313, 316, 317, 318, 322, 323, 324, 329, 330, 333, 334, 336, 337, 338, 347, 348, 349, 351, 354, 355, 356, 357, 358, 359, 360, 364, 366, 368, 369, 371, 372, 373, 377, 379, 381, 384, 386, 389, 391, 393, 398, 399}
p cnf 400 1764
305 134 -30 0
26 -174 -112 0
160 -349 -362 0
209 -374 319 0
-48 -190 -45 0
-388 266 135 0
217 60 -139 0
231 207 -192 0
-248 72 -160 0
127 -202 340 0
225 246 -339 0
227 -66 278 0
139 -224 -41 0
-1 -93 339 0
-115 285 -19 0
-71 -284 -320 0
-396 -74 13 0
-138 -99 -238 0
-197 -50 -169 0
252 226 -134 0
-255 388 76 0
223 -285 282 0
96 49 159 0
-226 32 -337 0
-91 386 -137 0
-294 -30 -230 0
-93 -16 -217 0
-200 19 -209 0
376 -280 -293 0
-391 -51 -238 0
-363 29 302 0
-30 92 117 0
-11 -133 126 0
-278 -328 -249 0
342 -272 169 0
-285 66 -228 0
366 180 19 0
-299 249 -386 0
265 -196 -157 0
143 -390 3 0
60 -231 21 0
-280 -124 16 0
311 346 -32 0
-171 46 -18 0
169 -378 170 0
-73 348 -280 0
170 -349 -134 0
325 -383 335 0
131 -307 -308 0
272 33 -39 0
70 361 -310 0
-374 43 -280 0
245 -204 353 0
-98 -147 233 0
-255 56 10 0
9 225 359 0
-209 112 -122 0
-367 281 -212 0
32 193 -238 0
74 390 151 0
-346 113 226 0
71 -355 -16 0
32 234 44 0
-130 -239 -50 0
-146 25 71 0
-293 194 -347 0
132 -397 116 0
-224 -233 -382 0
-194 73 -86 0
-174 73 291 0
85 219 234 0
-210 -152 260 0
-60 -169 -94 0
322 -57 108 0
348 129 53 0
331 -7 395 0
-26 199 -349 0
353 92 356 0
154 -237 -394 0
-100 176 42 0
317 -385 354 0
-41 334 -191 0
-237 -143 -148 0
241 93 182 0
22 210 28 0
-20 2 385 0
44 276 316 0
178 58 38 0
-96 341 -335 0
327 222 -55 0
393 92 -285 0
-249 182 81 0
-73 347 -226 0
310 71 378 0
-91 139 187 0
320 -127 -80 0
82 164 187 0
200 -376 304 0
-87 263 -121 0
-376 343 177 0
-114 378 101 0
-272 288 84 0
61 199 271 0
13 -224 343 0
243 -322 380 0
-142 -67 333 0
143 -259 13 0
-374 -217 -163 0
-314 -130 -90 0
326 -331 -139 0
-245 -30 -338 0
-119 125 -142 0
38 -164 171 0
287 -320 333 0
360 201 -165 0
-113 -315 245 0
384 231 -1 0
124 -237 -273 0
239 -149 216 0
-200 192 226 0
355 282 8 0
345 52 -198 0
271 391 -389 0
-32 354 63 0
179 -341 253 0
240 329 -239 0
-145 45 -55 0
376 -383 296 0
-400 -338 123 0
49 -37 78 0
-382 283 -128 0
57 -79 300 0
-154 103 -236 0
236 -146 -392 0
-87 363 -287 0
298 248 -390 0
-240 -143 -328 0
351 1 -209 0
382 128 -118 0
-362 -246 -124 0
213 -51 -228 0
214 76 -352 0
113 141 -400 0
62 -300 18 0
189 -221 388 0
178 -184 -13 0
168 351 -211 0
271 222 -308 0
348 41 295 0
291 113 -237 0
-231 -13 77 0
-303 134 -184 0
-201 104 227 0
-10 -96 279 0
-58 -89 -164 0
9 241 -324 0
-51 -103 -394 0
295 -379 48 0
-27 -140 -245 0
230 -295 364 0
308 -137 -244 0
297 336 247 0
-149 -231 111 0
-263 81 -35 0
-397 -44 -219 0
110 167 276 0
-277 -42 -272 0
118 375 185 0
-51 132 63 0
-187 222 185 0
-36 -52 -228 0
20 168 112 0
-111 -241 161 0
355 68 -243 0
-68 138 -121 0
160 -120 -329 0
106 281 -371 0
-327 384 333 0
-45 -215 -114 0
-345 -355 -184 0
-151 97 -111 0
114 -307 2 0
-199 -20 297 0
156 140 -43 0
240 291 -356 0
145 -235 -87 0
92 397 313 0
9 117 356 0
14 -222 36 0
-142 290 282 0
-213 114 -15 0
-221 -90 128 0
-8 -39 -295 0
211 -346 -274 0
-40 -262 137 0
-198 20 -150 0
-321 -305 98 0
-77 106 223 0
-312 -376 392 0
-38 -37 103 0
-64 170 28 0
156 101 -306 0
-332 -188 202 0
-34 356 -172 0
381 -19 -201 0
291 180 358 0
28 22 268 0
75 310 -107 0
-2 380 187 0
241 364 -64 0
-210 220 376 0
-89 -96 -123 0
271 292 183 0
322 -137 -46 0
75 -133 360 0
272 -180 326 0
26 32 -399 0
115 25 399 0
18 -216 189 0
357 -148 -345 0
259 -234 -22 0
97 -264 33 0
-48 -84 -152 0
351 -59 227 0
-33 149 -79 0
-27 -299 -100 0
-21 335 75 0
221 265 191 0
-133 -65 -89 0
-382 -164 -72 0
-99 8 -365 0
-368 300 -82 0
-62 241 257 0
-116 -134 -138 0
29 179 -27 0
260 -328 -314 0
112 -262 61 0
98 86 -20 0
264 185 -31 0
241 -39 -227 0
4 33 234 0
28 -361 -237 0
-312 166 328 0
167 -188 -344 0
-6 -21 375 0
223 -60 136 0
-140 127 -239 0
141 -15 -247 0
-348 -128 -8 0
202 -207 -159 0
187 -300 -341 0
342 303 240 0
309 139 -155 0
60 -78 -64 0
154 74 -330 0
374 180 378 0
-150 98 -239 0
-336 -97 -3 0
251 -224 361 0
-279 280 221 0
-385 -2 167 0
-95 -73 152 0
-19 -247 -161 0
43 333 13 0
369 -106 303 0
226 239 -87 0
216 219 302 0
160 -49 153 0
352 62 266 0
-259 -44 -263 0
-354 59 139 0
247 361 -147 0
-206 148 288 0
390 291 -73 0
-337 -149 -14 0
289 -351 -296 0
-253 199 111 0
-200 -23 277 0
365 67 -332 0
97 259 185 0
34 134 -228 0
-287 -112 -48 0
-360 -137 181 0
-209 74 -132 0
21 62 -328 0
-43 -190 382 0
-50 -312 -343 0
111 256 -198 0
13 -375 -245 0
123 -240 -398 0
277 141 28 0
319 -386 -326 0
158 -198 14 0
-294 227 193 0
-152 -358 -75 0
357 -274 -307 0
-20 42 -162 0
-388 -270 -58 0
-335 193 341 0
160 -134 297 0
177 16 129 0
-266 196 -111 0
181 -54 329 0
288 162 190 0
128 319 -52 0
56 233 -3 0
135 -81 -267 0
287 -81 373 0
-189 -294 350 0
261 310 256 0
194 -262 379 0
250 238 15 0
303 -259 -226 0
-362 -371 165 0
184 -58 39 0
100 -166 98 0
-10 -311 272 0
-181 209 -375 0
230 275 -79 0
34 -329 -214 0
216 -326 -213 0
152 137 -80 0
226 -359 321 0
78 34 214 0
290 253 251 0
373 -40 -294 0
-252 67 275 0
-91 199 -380 0
342 -64 -173 0
335 -390 -18 0
65 305 -271 0
-142 -130 225 0
47 227 151 0
-201 1 -251 0
321 116 155 0
66 -33 103 0
-176 75 390 0
287 -354 23 0
-188 -211 -323 0
270 47 -22 0
368 -164 284 0
-200 -365 364 0
347 236 -386 0
-240 377 361 0
-276 -120 94 0
-233 234 -309 0
-303 126 153 0
201 39 149 0
329 309 -316 0
-81 400 134 0
-352 -370 -53 0
-339 -23 -55 0
124 -220 -276 0
368 18 272 0
-111 -148 145 0
-251 -74 256 0
-68 295 -328 0
317 -136 -331 0
297 74 -360 0
349 -32 341 0
309 -343 -360 0
200 72 -385 0
133 -285 122 0
245 -97 311 0
295 59 -91 0
73 71 -193 0
-13 391 -298 0
-160 -19 -202 0
-84 392 351 0
108 355 -159 0
-175 291 -266 0
158 202 129 0
44 295 223 0
-330 8 -243 0
-144 260 256 0
-51 381 -161 0
-289 256 10 0
394 114 -79 0
117 247 225 0
92 -336 -116 0
-280 138 3 0
391 -160 217 0
57 209 189 0
117 135 -131 0
-383 393 -342 0
-396 85 297 0
-106 78 -63 0
-87 -199 -328 0
43 358 -231 0
281 357 -183 0
-175 155 45 0
-138 147 42 0
124 -175 20 0
368 102 128 0
329 -312 -47 0
-232 67 -260 0
-87 273 6 0
-374 -358 -127 0
-172 -51 -385 0
142 165 347 0
75 -6 145 0
-395 52 -224 0
-127 190 78 0
313 94 192 0
-321 243 -367 0
63 357 21 0
-18 -335 314 0
156 -294 -102 0
215 66 -161 0
376 240 -237 0
-65 103 76 0
-280 242 -323 0
103 -167 -67 0
233 -105 -129 0
92 -172 194 0
-257 -218 223 0
-198 -202 21 0
-87 111 180 0
316 372 -230 0
396 -368 313 0
247 213 -218 0
-292 -80 -324 0
338 357 280 0
-203 99 68 0
-6 -60 -241 0
-135 314 -69 0
325 76 -302 0
-311 -167 170 0
181 293 105 0
137 -336 261 0
-379 -139 -400 0
285 28 294 0
222 -1 -248 0
385 171 367 0
-103 36 371 0
165 1 328 0
-300 -205 -380 0
-392 292 284 0
264 -281 -335 0
-388 224 171 0
-390 -98 -242 0
251 1 -326 0
-4 -224 -218 0
-100 -322 -233 0
-282 -170 19 0
123 -213 345 0
56 280 -23 0
383 320 109 0
-181 -288 -178 0
-228 157 -387 0
266 21 -219 0
-288 47 85 0
235 -273 -182 0
268 44 -299 0
-202 344 205 0
-164 332 -40 0
100 -198 -162 0
213 -341 -19 0
213 -133 -204 0
-177 220 338 0
346 -127 192 0
-193 220 398 0
-317 -375 -368 0
221 -121 -228 0
-264 -385 -378 0
114 -345 288 0
-183 370 122 0
379 332 -38 0
-329 -343 -46 0
-59 331 42 0
110 215 100 0
398 52 321 0
-130 -45 312 0
-340 -389 168 0
21 196 176 0
26 117 -170 0
154 -308 -337 0
300 111 295 0
191 -344 297 0
52 386 394 0
-251 15 -205 0
144 -163 -183 0
-363 95 -240 0
216 -26 393 0
287 -353 -17 0
182 -139 -86 0
178 -244 -56 0
-309 292 -158 0
-156 -257 244 0
294 300 -222 0
282 307 -17 0
-317 -310 -260 0
-158 95 -123 0
-142 -204 -344 0
116 227 149 0
-325 39 -220 0
-75 -290 -147 0
-162 352 360 0
302 -285 78 0
393 -173 -298 0
-348 -70 -360 0
-46 -111 -213 0
187 101 -309 0
357 118 156 0
-67 114 -284 0
-27 -56 251 0
55 23 24 0
-324 -66 138 0
-376 385 -329 0
377 -280 392 0
-236 -119 -35 0
-171 89 11 0
161 -283 -129 0
214 313 343 0
-231 334 -119 0
175 -161 -383 0
121 -87 -333 0
62 383 372 0
41 297 -128 0
-17 39 97 0
-92 -326 31 0
-34 -348 -55 0
370 346 371 0
126 354 -60 0
319 -203 107 0
-391 147 39 0
-32 370 111 0
-143 -146 69 0
370 202 306 0
302 -76 -268 0
-395 56 -128 0
193 215 -295 0
306 304 349 0
-170 -151 -145 0
-288 93 -195 0
188 -82 151 0
-144 -47 79 0
393 -325 185 0
-341 -230 -315 0
-311 18 335 0
-235 96 -330 0
146 -233 185 0
-66 -362 33 0
203 -298 -264 0
-248 -159 -383 0
396 -239 291 0
-94 77 196 0
-172 339 -168 0
255 270 233 0
-336 -82 55 0
-220 395 -199 0
-180 160 316 0
-252 215 -288 0
-136 -91 74 0
7 -209 -381 0
157 -63 396 0
97 -49 387 0
-138 -385 -46 0
-65 -280 392 0
161 -113 323 0
338 -317 343 0
-349 -71 112 0
-337 -3 392 0
-334 -211 30 0
211 344 -233 0
-146 344 355 0
-360 -26 188 0
-361 89 -350 0
-315 248 -240 0
81 347 -153 0
-69 314 -369 0
-59 70 -290 0
-101 246 -330 0
-247 181 275 0
109 222 290 0
17 -92 -116 0
-361 -282 92 0
-10 -283 356 0
117 -212 -378 0
-269 308 -164 0
-156 319 -211 0
-32 -233 73 0
138 139 -145 0
-348 371 310 0
289 -196 -54 0
226 211 311 0
162 -327 -24 0
-152 247 200 0
167 -356 -266 0
-159 286 -180 0
192 -267 -331 0
359 -187 -271 0
-84 -331 -393 0
-335 1 334 0
90 12 50 0
-387 42 86 0
162 -382 -214 0
50 154 -55 0
44 377 72 0
-304 -342 279 0
36 173 -160 0
385 180 -217 0
146 369 -69 0
117 -263 -371 0
-45 -374 -394 0
364 -134 -228 0
118 257 196 0
38 -32 -13 0
-119 399 329 0
-275 158 -370 0
154 287 -168 0
45 16 187 0
397 -383 390 0
-286 119 -4 0
302 380 -142 0
-386 291 83 0
342 333 394 0
150 388 -153 0
344 -269 193 0
-309 -138 269 0
-195 -252 367 0
224 354 -86 0
-75 -397 -288 0
-348 -300 286 0
-171 281 -354 0
242 129 -238 0
-304 -241 82 0
309 -44 214 0
104 -385 95 0
345 341 135 0
-322 -12 145 0
179 5 -201 0
-395 147 -265 0
103 70 -42 0
87 -147 -72 0
107 365 19 0
5 -290 133 0
-206 93 -323 0
-76 110 388 0
216 41 222 0
-1 309 -245 0
194 -27 -388 0
-152 267 -79 0
-139 -163 135 0
-278 -323 272 0
-153 -4 174 0
348 -108 291 0
-305 -14 -114 0
-323 324 164 0
175 -104 296 0
-209 103 200 0
75 91 199 0
357 -189 -51 0
-232 -46 396 0
6 157 -48 0
-45 -310 195 0
161 196 327 0
-92 269 -297 0
-98 116 -65 0
-27 -192 311 0
305 -375 -227 0
-234 -398 54 0
-85 -110 -33 0
13 389 -270 0
187 227 302 0
85 -72 18 0
-300 -271 -115 0
350 49 -20 0
-297 391 331 0
26 -140 -271 0
270 54 -204 0
76 -203 -246 0
-181 384 261 0
136 94 -330 0
82 -382 36 0
177 8 -266 0
-130 162 313 0
-340 -359 -290 0
18 142 283 0
268 25 -167 0
-249 132 298 0
350 -371 281 0
102 170 77 0
-166 -161 -349 0
286 -14 -6 0
-141 259 -278 0
48 182 44 0
88 -333 -339 0
53 211 -268 0
162 -276 -221 0
304 -345 -58 0
299 -264 -331 0
-59 -25 94 0
147 37 -220 0
158 -371 137 0
-159 353 -177 0
-167 -382 69 0
-119 226 -353 0
-131 353 -253 0
103 -237 74 0
-80 -293 -309 0
266 -241 216 0
-324 333 -251 0
336 -150 -284 0
-278 -73 91 0
-101 348 -310 0
-213 20 -73 0
149 239 -186 0
-334 -75 -372 0
216 111 56 0
-375 -137 67 0
163 -100 313 0
-257 326 -337 0
327 -235 -363 0
251 306 -94 0
-230 -73 -291 0
-225 226 255 0
-382 156 100 0
-164 -345 -219 0
-188 -168 -315 0
-123 35 -84 0
-283 -51 164 0
-234 139 -340 0
-226 -167 -209 0
-200 27 30 0
312 -111 261 0
-176 -114 -100 0
-234 -225 -386 0
320 218 -260 0
-116 -341 360 0
-83 349 303 0
-253 -147 -288 0
-354 166 -263 0
-83 42 7 0
-116 -190 256 0
146 -312 -334 0
-16 -319 -210 0
-169 -222 -237 0
173 -183 -269 0
-300 164 57 0
-145 -298 -348 0
-278 399 -9 0
106 87 210 0
-345 355 284 0
-57 -229 -207 0
-148 -379 274 0
144 -26 174 0
-37 -106 369 0
368 -361 -301 0
395 97 69 0
-294 60 -148 0
-122 -266 -259 0
83 127 100 0
75 273 -394 0
24 295 59 0
-268 377 -384 0
194 -376 -98 0
139 -324 -166 0
-151 340 -208 0
4 -71 -143 0
-317 -60 -111 0
357 -127 -366 0
-63 -143 36 0
-346 60 161 0
-290 -355 27 0
330 -351 -61 0
362 -45 388 0
358 -320 330 0
-100 -205 -368 0
-310 230 214 0
251 325 87 0
-62 -339 -252 0
86 -327 51 0
-370 172 -216 0
67 210 345 0
-168 44 375 0
-223 264 -95 0
283 308 66 0
184 33 13 0
244 152 -343 0
-195 159 395 0
43 -254 128 0
59 -116 -316 0
-185 -236 13 0
271 -2 273 0
180 -289 278 0
-381 384 206 0
-229 -307 27 0
-13 16 -8 0
-88 -158 19 0
-157 45 313 0
292 26 64 0
-77 -145 -126 0
139 96 38 0
-379 -374 376 0
-329 -292 -168 0
381 -159 -84 0
-177 -251 240 0
-216 343 -44 0
-125 351 261 0
-231 247 184 0
-93 -90 -53 0
-52 47 -231 0
207 92 365 0
370 -156 -379 0
-190 388 -207 0
93 -179 -114 0
7 168 278 0
276 299 -18 0
287 -30 -28 0
231 -71 233 0
339 336 105 0
335 -34 -389 0
19 -119 117 0
361 -243 41 0
228 -101 115 0
372 -138 350 0
398 207 280 0
389 68 -192 0
227 -379 342 0
284 -285 -294 0
-267 -163 59 0
388 178 -36 0
246 -311 -379 0
-69 -185 -351 0
369 39 -138 0
-189 -17 -141 0
-198 361 200 0
306 31 -250 0
129 -174 120 0
317 -7 391 0
-51 175 386 0
144 -109 117 0
385 155 23 0
-1 -238 113 0
67 25 -157 0
139 -11 246 0
233 -226 106 0
9 313 359 0
219 158 56 0
-160 -280 387 0
-227 -369 -232 0
358 323 191 0
-192 140 271 0
33 -8 25 0
-229 86 271 0
-46 -17 399 0
-333 -359 73 0
95 -17 106 0
-298 -98 -126 0
393 -322 374 0
-394 -322 192 0
165 335 82 0
-120 -90 43 0
-276 42 -9 0
-180 257 -77 0
-342 -58 183 0
-135 -351 -60 0
305 209 -328 0
-394 322 -177 0
375 227 198 0
215 353 375 0
-362 -131 294 0
110 65 -271 0
-106 47 170 0
-316 -246 -361 0
304 276 -197 0
335 -182 -236 0
29 74 -221 0
370 161 -326 0
-238 164 -156 0
176 -294 159 0
-173 164 -172 0
47 -398 -217 0
-206 -127 -377 0
385 -390 -330 0
-282 370 -236 0
250 265 -287 0
347 386 61 0
49 173 202 0
339 213 -168 0
-232 -271 8 0
-317 258 70 0
126 -127 281 0
-289 262 -92 0
-374 55 -208 0
312 272 -400 0
326 -255 93 0
-11 -182 174 0
311 276 213 0
275 -124 -144 0
-62 217 -377 0
122 -26 274 0
183 -367 255 0
193 -315 -270 0
-220 161 -108 0
-1 107 226 0
-305 -230 399 0
292 -152 204 0
-69 -283 -171 0
246 -100 220 0
-360 -184 312 0
-148 224 -328 0
-178 -251 -392 0
-323 62 111 0
-388 177 -104 0
-393 292 39 0
86 78 54 0
-154 186 -391 0
390 236 -148 0
-230 -318 10 0
-223 209 -372 0
-16 52 -213 0
-375 77 -167 0
352 137 370 0
20 -241 -71 0
-113 -263 84 0
-397 211 -400 0
309 -33 -76 0
86 -225 -383 0
114 381 -312 0
-350 -160 295 0
181 -46 -286 0
-269 -204 10 0
-305 50 -74 0
-51 315 -98 0
9 -84 288 0
-351 20 359 0
-153 -45 -10 0
91 -105 125 0
-220 296 -45 0
340 -335 -205 0
35 108 -335 0
-29 -397 17 0
141 -384 394 0
-329 281 -347 0
-357 372 346 0
235 -196 -372 0
-168 163 137 0
205 361 -368 0
371 -50 306 0
362 250 128 0
-107 280 134 0
-9 -135 180 0
-119 85 166 0
125 -9 236 0
162 96 -223 0
65 -63 344 0
14 317 203 0
-33 -93 64 0
-74 -164 399 0
-313 181 70 0
-4 -228 396 0
82 54 392 0
-373 -55 -174 0
-308 355 273 0
-321 395 255 0
236 376 57 0
-273 345 100 0
-310 -374 -7 0
383 214 -120 0
278 99 212 0
72 -103 -329 0
107 221 -275 0
-381 -118 123 0
9 88 74 0
-279 -344 -282 0
131 125 -238 0
323 227 167 0
-263 242 -144 0
316 192 150 0
182 -157 -341 0
-366 365 333 0
-399 -144 -28 0
-323 289 366 0
313 296 -209 0
398 -234 58 0
359 362 -66 0
101 33 -368 0
-124 217 122 0
226 178 -188 0
-348 -27 115 0
5 -245 69 0
287 -3 117 0
41 275 -218 0
-27 233 362 0
-59 78 33 0
-100 73 360 0
312 100 -216 0
159 169 -35 0
77 260 198 0
-51 -227 -155 0
95 -50 -109 0
223 179 -292 0
-2 290 32 0
-37 221 -373 0
-183 86 92 0
379 -217 -113 0
-291 144 71 0
-275 -296 -265 0
-107 -309 334 0
46 152 333 0
-234 -227 105 0
333 243 -142 0
-94 -83 -367 0
-388 273 -55 0
-105 295 -77 0
346 -276 273 0
290 107 -124 0
-191 342 -108 0
-216 -378 -312 0
159 -72 -394 0
189 89 -244 0
-305 -28 392 0
-35 -356 394 0
147 304 392 0
367 -341 -377 0
127 256 330 0
-315 -220 -84 0
256 -316 -17 0
-272 179 214 0
-108 104 41 0
-113 302 89 0
198 212 -12 0
-253 313 -180 0
-132 -303 108 0
-332 33 -343 0
-104 -282 17 0
-28 -181 96 0
169 -241 -221 0
-350 -213 125 0
-75 -171 209 0
-324 285 -125 0
-315 -390 324 0
-310 -360 -324 0
109 303 -375 0
-187 -279 -50 0
-255 272 -176 0
283 343 3 0
-350 31 349 0
-278 134 80 0
388 -197 -8 0
-336 -112 -223 0
-202 337 -313 0
57 -118 -267 0
226 268 -394 0
-279 -325 257 0
105 -225 268 0
47 -32 177 0
231 -232 -209 0
334 -383 -86 0
-160 338 217 0
128 391 361 0
-173 284 -17 0
-257 171 -102 0
172 199 -123 0
-215 321 109 0
-68 -8 -250 0
-51 -90 -177 0
-62 373 -325 0
-136 343 194 0
-332 -129 -23 0
-224 -352 194 0
-365 329 -214 0
-164 48 392 0
178 56 -86 0
-97 53 191 0
-71 347 276 0
128 -188 165 0
-117 12 284 0
147 -354 21 0
-45 -234 324 0
274 177 381 0
-14 48 188 0
89 -219 -149 0
-251 -388 236 0
-272 -176 245 0
-296 -305 -121 0
243 -381 -322 0
-144 -183 -206 0
284 -367 182 0
-245 -210 350 0
-142 -133 -317 0
-322 373 295 0
216 369 210 0
1 -223 260 0
303 -159 -358 0
216 160 -36 0
-102 268 -77 0
-100 314 -389 0
-263 138 -58 0
-120 347 -397 0
-179 380 -400 0
400 345 89 0
366 -262 -299 0
-305 -350 272 0
49 -306 -390 0
-132 -279 -56 0
329 263 -301 0
232 371 107 0
32 368 250 0
-10 -375 -225 0
-360 -342 305 0
97 -62 55 0
243 151 -221 0
-278 283 42 0
211 -321 61 0
-157 -262 208 0
210 71 272 0
263 370 -254 0
293 227 120 0
399 -189 303 0
340 -3 329 0
125 270 -238 0
394 -387 -61 0
243 101 -282 0
167 297 -122 0
-82 -191 184 0
51 -167 224 0
287 321 108 0
291 251 196 0
309 -194 130 0
277 261 -66 0
130 237 -213 0
-397 296 148 0
-114 -267 217 0
366 294 242 0
-258 -171 162 0
91 -110 -371 0
-277 -18 280 0
334 125 369 0
62 -51 -154 0
-273 -296 268 0
74 194 284 0
28 -98 -253 0
-219 -267 -3 0
-134 -166 -26 0
-333 289 -382 0
-231 265 -181 0
221 -213 -28 0
241 -38 -305 0
289 264 -62 0
336 70 23 0
-60 -96 274 0
384 155 134 0
178 -391 -382 0
154 -346 285 0
-289 -257 386 0
-267 -37 330 0
131 -276 -366 0
-116 64 -196 0
-45 -74 -380 0
-130 -136 371 0
-47 320 -212 0
333 373 368 0
-129 -11 -59 0
-33 45 185 0
-228 -224 251 0
-231 20 327 0
-43 133 328 0
-394 313 47 0
-50 -183 -386 0
-182 194 95 0
228 -343 -271 0
171 -337 277 0
-195 -24 -249 0
-340 246 -168 0
-326 -382 -204 0
178 13 372 0
-138 -392 90 0
252 196 150 0
-344 -394 -370 0
-168 61 -116 0
-306 -197 334 0
-19 372 149 0
76 88 277 0
-225 9 -135 0
-125 307 -68 0
22 -58 -308 0
197 -249 97 0
96 -103 292 0
226 96 -385 0
-93 -231 28 0
306 206 186 0
-325 -33 -185 0
-151 -10 -107 0
78 -162 -243 0
-154 263 -364 0
282 108 -281 0
258 -137 361 0
8 184 -110 0
-269 -268 -55 0
122 -343 -243 0
305 -339 -249 0
214 -311 260 0
-132 97 -245 0
250 -378 -83 0
-61 -356 272 0
19 -144 244 0
-138 -163 316 0
12 -258 -156 0
-217 136 82 0
58 -304 -20 0
275 -11 -262 0
-230 123 204 0
281 9 134 0
-380 -155 230 0
-169 -18 -14 0
-331 -63 182 0
140 -334 346 0
-260 -125 78 0
19 -198 225 0
183 50 -221 0
294 212 -38 0
120 -230 -10 0
344 -248 -161 0
58 -99 -114 0
-292 -364 -183 0
365 -211 -126 0
-314 -28 -222 0
-49 -6 232 0
-65 230 -217 0
22 260 -88 0
128 267 -176 0
387 -53 -175 0
348 -9 -291 0
207 101 60 0
223 -353 105 0
-91 158 -103 0
344 -400 7 0
-162 300 132 0
-369 258 -147 0
-328 -7 239 0
-272 -31 -209 0
-321 -303 353 0
-315 89 -86 0
366 125 151 0
-227 18 126 0
200 277 213 0
-251 68 -65 0
228 387 -329 0
53 348 339 0
-270 -1 341 0
351 356 31 0
149 -104 -194 0
8 302 7 0
204 328 -44 0
349 301 -124 0
-154 -324 -315 0
74 -301 49 0
-99 -160 -257 0
-245 -352 182 0
-120 -238 231 0
247 373 -307 0
30 -53 246 0
169 -200 -289 0
-259 -345 -135 0
-187 209 108 0
-122 390 -338 0
343 -43 -276 0
-396 -48 254 0
-73 121 281 0
-346 74 305 0
-35 -173 -166 0
366 58 -219 0
-239 -5 -244 0
7 -154 312 0
145 -114 -358 0
303 240 -373 0
-262 -231 128 0
133 113 40 0
189 391 76 0
-305 -47 -28 0
3 31 385 0
-217 186 -166 0
-281 -159 73 0
-197 4 -124 0
-386 144 -307 0
97 -19 168 0
-215 -63 -40 0
344 -388 106 0
142 265 -144 0
-394 373 -206 0
124 391 109 0
-334 -53 -255 0
-178 103 -177 0
338 -105 -206 0
-327 -239 -89 0
-77 -298 266 0
278 -214 -378 0
-381 -314 -138 0
61 275 -389 0
-344 347 -20 0
-369 92 -270 0
-358 11 218 0
-392 -104 388 0
-41 328 299 0
-173 -307 319 0
-209 177 319 0
-140 351 -56 0
38 -349 -191 0
-91 -226 141 0
233 281 277 0
323 -259 -22 0
43 -211 312 0
-290 145 -183 0
167 40 -64 0
397 33 149 0
60 114 -203 0
39 257 371 0
-318 -253 -54 0
-212 -180 -113 0
-340 -12 -197 0
-141 -255 -113 0
-144 169 180 0
204 -347 248 0
208 169 -28 0
-166 -98 -392 0
-311 -218 279 0
386 -355 188 0
-111 -302 26 0
-109 91 400 0
337 -133 197 0
-394 13 -385 0
-151 286 114 0
100 -349 -193 0
266 -396 -72 0
335 -86 219 0
353 -219 -66 0
-84 111 -336 0
139 63 145 0
276 184 51 0
344 134 72 0
101 309 -120 0
-196 -311 -119 0
395 -312 -314 0
189 -376 -98 0
37 -352 75 0
-308 -17 115 0
14 183 399 0
47 8 -75 0
11 124 121 0
369 -115 262 0
318 -230 -240 0
-396 387 114 0
145 116 -204 0
144 45 61 0
268 -188 248 0
54 83 104 0
75 -100 -146 0
104 57 226 0
392 381 -96 0
185 272 -353 0
336 -60 19 0
284 308 235 0
8 294 66 0
208 -6 -279 0
-181 368 273 0
-352 -217 269 0
-130 -112 -354 0
322 261 -84 0
152 200 76 0
332 -270 261 0
327 -29 -246 0
-328 -179 -113 0
-55 194 -328 0
-83 -133 363 0
379 -215 -167 0
170 140 -5 0
113 237 310 0
119 87 280 0
-370 -126 286 0
-292 307 17 0
208 -42 132 0
310 227 250 0
-344 -86 220 0
62 5 205 0
-75 31 -183 0
133 167 171 0
-90 -154 194 0
-399 -237 -254 0
-345 -361 -188 0
-113 314 283 0
-79 -380 146 0
-377 221 -267 0
-222 -2 -167 0
-136 -249 209 0
40 316 -370 0
-328 -74 31 0
-263 38 -365 0
66 323 214 0
-5 -239 -182 0
-153 245 287 0
-392 -105 -60 0
35 34 134 0
-89 310 -200 0
-251 -165 76 0
-63 141 291 0
-325 317 -397 0
-214 -23 -79 0
-382 -342 368 0
-50 189 218 0
140 -95 376 0
-86 -325 -126 0
-89 156 -252 0
-19 -133 300 0
-176 -78 121 0
-218 -154 -208 0
39 76 391 0
-339 -199 -306 0
-87 329 313 0
280 -326 227 0
-274 370 395 0
56 -67 -276 0
325 98 374 0
-321 -188 -255 0
-197 282 354 0
267 -26 320 0
-5 296 342 0
-239 -178 -363 0
-208 72 271 0
20 320 30 0
-273 285 -392 0
-163 42 19 0
-23 -327 94 0
169 395 -389 0
-269 195 202 0
-334 -90 44 0
-341 348 -274 0
129 89 345 0
-230 -200 355 0
47 -105 -75 0
66 373 201 0
-110 -154 255 0
-356 -362 352 0
-369 -284 138 0
-239 338 232 0
-242 -383 42 0
184 -212 -149 0
339 -67 -247 0
218 -293 -6 0
-140 -4 331 0
174 226 267 0
-230 1 360 0
177 29 -275 0
-47 -288 108 0
193 132 201 0
284 147 -232 0
329 -180 221 0
-110 123 45 0
40 -360 -205 0
-336 -245 42 0
-194 86 -227 0
385 78 87 0
-100 146 -320 0
5 -202 13 0
154 36 147 0
-278 392 -206 0
-120 -162 -220 0
-288 381 291 0
-353 65 80 0
395 -220 256 0
-328 -367 163 0
-152 184 209 0
1 -39 215 0
-45 27 312 0
-82 -375 148 0
78 -43 -250 0
-76 179 -24 0
40 82 115 0
-250 -37 139 0
116 -175 -241 0
-190 154 -326 0
379 22 -21 0
-292 -394 6 0
-128 -314 -276 0
362 268 -282 0
361 -394 397 0
-141 -238 -62 0
-55 77 -240 0
-2 -270 -246 0
-305 385 193 0
-352 -58 -333 0
-325 -144 169 0
235 396 -249 0
-257 238 348 0
-40 267 98 0
125 -335 40 0
117 -382 -233 0
243 -208 329 0
48 -106 -243 0
14 180 -46 0
-211 -142 -271 0
399 376 23 0
-199 72 270 0
273 305 171 0
-350 122 270 0
-150 -48 -337 0
185 -99 162 0
101 -124 -198 0
-156 321 301 0
-130 -186 -294 0
-178 -73 -92 0
-359 -157 -243 0
203 133 -171 0
10 167 166 0
388 -78 -252 0
338 400 -331 0
-36 -123 -297 0
-68 -251 -166 0
20 -283 -394 0
343 276 -363 0
137 -296 215 0
10 368 -37 0
-107 -115 -281 0
383 -242 246 0
279 180 -245 0
-116 -218 230 0
283 -375 17 0
115 -400 391 0
-6 40 -302 0
275 -374 101 0
370 -263 -275 0
83 73 -55 0
-386 124 -215 0
-164 -28 363 0
200 -185 391 0
317 -203 173 0
-296 -99 98 0
-299 357 -117 0
35 -97 -12 0
394 272 -30 0
-222 89 121 0
-361 -240 -100 0
-179 -373 -144 0
122 -255 -322 0
-239 -335 48 0
42 98 149 0
145 221 57 0
-196 15 -330 0
-116 -288 285 0
-25 134 -221 0
-173 178 204 0
-395 -264 -362 0
-270 168 -92 0
324 275 362 0
359 310 -272 0
220 -318 -15 0
-342 -122 286 0
-203 32 188 0
-188 -100 -70 0
-253 201 -146 0
32 -139 -133 0
-185 250 -364 0
207 -369 -141 0
-173 40 -249 0
-48 -276 140 0
348 223 -226 0
-24 -219 396 0
-146 -185 -310 0
-274 187 -268 0
-246 -77 103 0
82 -322 319 0
-123 110 236 0
-270 -198 -193 0
270 338 164 0
224 215 -74 0
304 -99 310 0
-5 -202 174 0
-17 -82 399 0
74 287 -123 0
-366 -188 -55 0
-129 283 150 0
-230 226 -7 0
-223 -61 -250 0
325 48 147 0
-304 66 -307 0
-221 39 -294 0
-63 97 -79 0
254 205 -342 0
-16 25 -203 0
-132 42 -242 0
379 -369 -377 0
-20 356 -392 0
-381 -37 -56 0
192 118 -262 0
-273 312 -103 0
-360 63 297 0
-205 -263 211 0
-141 -319 341 0
206 27 35 0
-188 28 216 0
-261 323 248 0
-339 -19 367 0
148 220 -73 0
349 20 -253 0
222 21 -196 0
-296 376 -393 0
-86 -365 333 0
209 341 -161 0
-289 -343 -400 0
11 -26 -154 0
97 -182 -334 0
313 145 325 0
127 85 235 0
-63 -40 -291 0
-339 178 -3 0
-120 -392 -44 0
229 -320 -199 0
-145 12 74 0
96 51 68 0
100 15 -250 0
215 -360 -39 0
204 372 -262 0
-400 295 -326 0
239 20 -303 0
358 -91 -313 0
-255 93 236 0
-42 174 232 0
-302 -78 77 0
-349 -250 -204 0
142 240 -53 0
133 -348 177 0
99 -68 69 0
-214 54 -91 0
346 -43 -4 0
383 -342 120 0
-188 334 279 0
331 367 238 0
-291 -66 -88 0
226 198 83 0
-128 -217 273 0
-251 204 125 0
277 18 -237 0
-394 -81 -305 0
-26 74 361 0
245 153 -279 0
-168 -61 -249 0
-168 6 331 0
44 22 -150 0
-41 342 -315 0
-278 324 246 0
-94 -157 142 0
-300 -306 -73 0
-325 112 -190 0
299 -229 150 0
198 106 -52 0
-262 -82 -344 0
298 -78 -356 0
-62 182 -74 0
-246 190 -325 0
-253 88 216 0
-77 -205 -313 0
-152 384 241 0
-219 363 -211 0
383 232 -122 0
-232 -343 36 0
200 321 -25 0
-399 346 -390 0
369 -73 -225 0
-317 146 -162 0
336 75 -10 0
251 -83 -59 0
220 63 214 0
147 -28 -281 0
-122 376 51 0
-205 136 151 0
-281 50 217 0
-211 192 188 0
96 344 60 0
-334 379 -290 0
115 -7 58 0
-360 263 -262 0
362 292 -10 0
-158 151 -375 0
-116 248 167 0
-145 -260 327 0
-318 107 150 0
75 343 -293 0
-335 -342 371 0
-118 -158 -365 0
66 391 185 0
-323 321 30 0
-220 52 -3 0
-57 220 310 0
364 -64 -123 0
249 110 193 0
-215 147 232 0
-10 180 270 0
168 82 -66 0
175 46 -7 0
64 296 263 0
-290 3 330 0
169 332 -324 0
30 56 250 0
-214 -115 -17 0
50 279 -234 0
-213 1 235 0
-208 -345 139 0
-389 338 251 0
-225 117 -167 0
-155 -394 -185 0
135 -319 -328 0
89 -120 166 0
-62 -80 235 0
214 96 -366 0
-65 -389 21 0
266 116 194 0
-356 91 209 0
287 311 -120 0
372 -113 362 0
-126 306 340 0
307 187 -130 0
280 -347 -55 0
-78 -129 -115 0
-338 -328 396 0
68 387 201 0
9 -343 -128 0
295 62 72 0
-20 61 -193 0
-154 110 -116 0
271 -362 390 0
130 -383 -144 0
-168 354 -65 0
312 255 -222 0
72 346 -75 0
-256 215 124 0
-334 -241 -9 0
-59 -35 27 0
216 -331 -304 0
-262 -69 7 0
108 -254 -365 0
289 -103 63 0
-302 338 9 0
141 -373 120 0
206 84 375 0
-192 297 -17 0
168 370 291 0
280 -69 -377 0
-6 29 289 0
-73 213 -345 0
-42 94 -5 0
74 359 -144 0
-218 -395 -137 0
-400 -75 311 0
128 205 -138 0
74 241 369 0
-221 356 386 0
235 -161 -110 0
163 -295 -246 0
-15 358 238 0
-383 -277 -358 0
108 373 101 0
21 184 51 0
298 371 280 0
-68 -52 211 0
-340 -203 228 0
254 375 105 0
-47 125 296 0
-398 171 -303 0
16 133 -275 0
-15 -255 106 0
28 41 -106 0
-298 -154 -396 0